A, B:es_realizer{i:l}, P, Q:(ES{i}Prop{i'}).
A ||-{i} es.P(es)  B ||-{i} es.Q(es)  R-compat{i:l}(A; B)  A  B ||-{i} es.P(es) & Q(es) 

latex

Definitions	R ||- es.P(es), left  right, A || B, x:AB(x), R-Feasible(R), x(s), f(a), x:AB(x), ES, Prop, Type, Realizer, Top, x:A. B(x), Void, Consistent(R;es), es realizer ind Rplus compseq tag def, P  Q, t  T, P & Q, x:A. B(x)
Lemmas	R-Feasible-Rplus, es realizer wf, event system wf, R-consistent wf, R-Feasible wf, R-compat wf, Rplus wf